Termination w.r.t. Q proof of TRS/secret06sumList.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

IF₆(false, false, y, xs, ys, x) -> SUMLIST₂(ys, x)
P₁(s₁(s₁(x))) -> P₁(s₁(x))
SUMLIST₂(xs, y) -> P₁(head₁(xs))
SUMLIST₂(xs, y) -> HEAD₁(xs)
SUMLIST₂(xs, y) -> TAIL₁(xs)
IF₆(false, true, y, xs, ys, x) -> SUMLIST₂(xs, y)
SUMLIST₂(xs, y) -> INC₁(y)
SUMLIST₂(xs, y) -> ISZERO₁(head₁(xs))
SUMLIST₂(xs, y) -> ISEMPTY₁(xs)
SUM₁(xs) -> SUMLIST₂(xs, 0)
INC₁(s₁(x)) -> INC₁(x)
SUMLIST₂(xs, y) -> IF₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF₆(false, false, y, xs, ys, x) -> SUMLIST₂(ys, x)
P₁(s₁(s₁(x))) -> P₁(s₁(x))
SUMLIST₂(xs, y) -> P₁(head₁(xs))
SUMLIST₂(xs, y) -> HEAD₁(xs)
SUMLIST₂(xs, y) -> TAIL₁(xs)
IF₆(false, true, y, xs, ys, x) -> SUMLIST₂(xs, y)
SUMLIST₂(xs, y) -> INC₁(y)
SUMLIST₂(xs, y) -> ISZERO₁(head₁(xs))
SUMLIST₂(xs, y) -> ISEMPTY₁(xs)
SUM₁(xs) -> SUMLIST₂(xs, 0)
INC₁(s₁(x)) -> INC₁(x)
SUMLIST₂(xs, y) -> IF₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 7 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INC₁(s₁(x)) -> INC₁(x)

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

INC₁(s₁(x)) -> INC₁(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(INC₁(x₁)) = 1 + x₁²
POL(s₁(x₁)) = 1 + x₁²

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P₁(s₁(s₁(x))) -> P₁(s₁(x))

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

P₁(s₁(s₁(x))) -> P₁(s₁(x))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(P₁(x₁)) = x₁²
POL(s₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF₆(false, false, y, xs, ys, x) -> SUMLIST₂(ys, x)
IF₆(false, true, y, xs, ys, x) -> SUMLIST₂(xs, y)
SUMLIST₂(xs, y) -> IF₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
sumList₂(xs, y) -> if₆(isEmpty₁(xs), isZero₁(head₁(xs)), y, tail₁(xs), cons₂(p₁(head₁(xs)), tail₁(xs)), inc₁(y))
if₆(true, b, y, xs, ys, x) -> y
if₆(false, true, y, xs, ys, x) -> sumList₂(xs, y)
if₆(false, false, y, xs, ys, x) -> sumList₂(ys, x)
sum₁(xs) -> sumList₂(xs, 0)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.